/*
Frank
CAU
2019/11/23
*/
/**
 *对树进行操作 
**/
#include "functions.h"

void check_format(node *root)
{ //对整棵树进行修补和改造
    //TODO
}
void elim_c(node *cd)
{ //细节处理方法，供下面调用
    if (cd->_sym != '>')
    {
        return;
    }
    // 是蕴含逻辑
    // 变为析取
    cd->_sym = '!';

    if ((cd->_lc == null) || (cd->_rc == null))
    { //公式错误
        printf("消去蕴含出错,在节点");
        show(cd);
        printf("附近\n");

        error(ERR_BADFMT, cd);
    }
    // info
    printf("消去蕴含: 左子节点");
    show(cd->_lc);
    printf("右子节点");
    show(cd->_rc);
    printf("\n");

    // node *leftneg = new_rawneg();
    // cd->_lc->parent = leftneg;
    // leftneg->_lc = cd->_lc;
    // cd->_lc = leftneg;
    // leftneg->parent = cd;
    cd->_lc->neg(); //否定左孩子
}
void elim_conds(node *root) throw()
{ //消去蕴含符号
    // 异常直接抛出
    // 层序遍历
    printf("************消去蕴含符号************\n");
    hierarchical_traverse(root, elim_c);
}

void reduce_nega_scope(node *root)
{ //减少否定符号的辖域
    printf("************缩小否定辖域************\n");
    hierarchical_traverse(root, push_neg_down);
}

bool *g_invalid_alpha;
queue<same_alpha *> *g_waiting_list;
same_alpha *vars_in_region;

void check_prid_contain(node *prid, char old_alpha, char new_alpha)
{ //检查谓词节点的是否包含需要替换的变量
    // 改变量词辖域内相关的变量值为new_alpha
    // vars_in_region = new same_alpha();
    // 已经初始化完成
    if (prid->_type != N_PRID)
    {
        return;
    }
    // 是谓词
    if (prid->_vars != null)
    {
        printf("\t\t正在考察谓词");
        show(prid);
        // 考察谓词参数列表
        variable *v = prid->_vars;
        while (v != null)
        {
            if (v->_v == old_alpha)
            {
                // 这个变量需要替换
                show(prid);
                printf("需要替换%c为%c\n", old_alpha, vars_in_region->new_var);
                // variable* v
                vars_in_region->append(v);
                return;
            }
            v = v->_next_v;
        }
        // 未找到相关变量
        printf("未找到相关变量\n");
    }
    else
    {
        printf("\t\t谓词出错");
        error();
    }
}
void register_var(node *qt, char old_alpha, char new_alpha)
{ //登记
    // 改变量词辖域内所有的变量值
    hierarchical_traverse(qt, check_prid_contain, old_alpha, new_alpha);
}

void uniquify_qunt_var(node *quant)
{ //检查量词是否需要修改变量名

    if (quant->_type != N_QUANT)
    {
        // 不做处理
        return;
    }

    // 检查
    char var = get_var(quant->_vars);
    // 得到字母表当中的索引
    int idx = var - 'a';
    if (g_invalid_alpha[idx] == false)
    {
        // 可用
        printf("\t\t量词");
        show(quant);
        printf("变量尚可使用\n");

        g_invalid_alpha[idx] = true; // 占用
        return;
    }
    else
    {
        // 分配一个空闲字母
        printf("\t\t");
        show(quant);
        printf("该量词辖域需要替换变量\n");
        char new_alpha = get_var(quant->_vars);
        while (true)
        {
            if (g_invalid_alpha[idx] == true)
            { //无效，继续寻找

                printf("\t\t变量%c已被使用\n", idx + 'a');
                idx++;
            }
            else
            {
                g_invalid_alpha[idx] = true; //占用
                //带着找到的空闲字母，退出循环
                new_alpha = (char)('a' + idx);
                printf("\t\t找到空闲变量%c\n", new_alpha);
                break;
            }
            if (idx == ('z' - 'a'))
            { //到头了
                // 重置
                printf("重置idx到0");
                idx = 0;
            }
            if ((char)(idx + 'a') == var)
            { //循环一圈
                printf("变量过多");
                error();
            }
        }
        // 登记辖域之内需要替换的变量
        vars_in_region = new same_alpha(new_alpha);
        printf("添加一个量词");
        show(quant);
        printf("\n");
        // 一定首先把量词本身添加进列表去
        vars_in_region->append(quant->_vars);
        // 旧变量：var
        register_var(quant, var, new_alpha);
        // 注意，堆区的内存没有释放，这种返回应该是合理的
        g_waiting_list->push(vars_in_region);
        return;
    }
}
void change_var(queue<same_alpha *> *q)
{
    same_alpha *vs;
    while (!q->empty())
    {
        printf("\t\t**一个变量替换队列**");
        vs = q->front();
        // vs是一群需要替换变量
        char new_alpha = vs->new_var;
        list<variable *> *vl = vs->v_ptrs;
        list<variable *>::iterator iter;
        for (iter = vl->begin(); iter != vl->end(); iter++)
        {
            printf("替换一个%c", (*iter)->_v);
            (*iter)->_v = new_alpha;
        }
        q->pop();
        printf("\n");
    }
}
void delete_all(queue<same_alpha *> *q)
{
    same_alpha *t;
    while (!q->empty())
    {
        t = q->front();
        q->pop();
        delete t;
    }
}

void standardize_vars(node *root)
{

    printf("************变量标准化***********\n");
    // 不同的约束，采用不同的变量

    // TODO 去除无效约束
    // 并且报告错误
    // (@x)((@x)) 等四种组合

    // 假定约束均有效
    // (@x)(#y)(    P(x,y) ! ~Q(z)  )
    // const char *letters = "abcdefghijklmnopqrstuvwxyz";
    // 在堆区初始化一个数组
    g_invalid_alpha = new bool[26]{0};
    g_waiting_list = new queue<same_alpha *>;
    hierarchical_traverse(root, uniquify_qunt_var);
    change_var(g_waiting_list);
    // 释放堆区
    delete g_invalid_alpha;
    // 删除队列的时候，其中的对象会被释放吗？
    delete_all(g_waiting_list);
    delete g_waiting_list;
}

void delete_allqunt(node *all)
{
    if (all->_type == N_QUANT && all->_rc == null && all->_lc != null && all->parent != null)
    {                      //全称量词
        delete_merge(all); // 删除
    }
}
void erase_allqunt(node *root)
{ //消去全称量词
    printf("************消去全称量词***********\n");
    hierarchical_traverse(root, delete_allqunt);
}

void or2And(node *wedge)
{ //析取式
}
void convert2CNF(node *root)
{ //化为合取范式
    hierarchical_traverse(root, or2And);
}